(*
 * Copyright 2014, General Dynamics C4 Systems
 *
 * SPDX-License-Identifier: GPL-2.0-only
 *)

chapter "Specifications"

(*
 * List of rules to make various images.
 *
 * Some rules have duplicate targets of the form:
 *
 *    theories [condition = "MOO", quick_and_dirty]
 *       "foo"
 *    theories
 *       "foo"
 *
 * The idea is that if the environment variable "MOO" is defined we
 * execute the first rule (doing the proof in quick-and-dirty mode), and
 * then find we need not take any action for the second. Otherwise, we
 * skip the first rule and only perform the second.
 *)

(*
 * Abstract Specification
 *)

(* Session on which most other sessions build. *)
session ASpec in "abstract" = Word_Lib +
  options [document=pdf]
  sessions
    "HOL-Library"
    Lib
    ExecSpec
  directories
    "$L4V_ARCH"
  theories
    "Syscall_A"
    "Intro_Doc"
    "Glossary_Doc"
    (* "KernelInit_A" *)
  document_files
    "VERSION"      (* generated by `make ASpec` *)
    "git-root.tex" (* generated by `make ASpec` *)
    "root.tex"
    "root.bib"
    "defs.bib"
    "ulem.sty"
    "imgs/CDT.pdf"
    "imgs/seL4-background_01.pdf"
    "imgs/seL4-background_03.pdf"
    "imgs/seL4-background_04.pdf"
    "imgs/sel4objects_01.pdf"
    "imgs/sel4objects_05.pdf"
    "imgs/sel4_internals_01.pdf"
  document_files (in "document/$L4V_ARCH")
    "ARCH.tex"

(*
 * Executable/Design Specification
 *)

session ExecSpec in "design" = Word_Lib +
  options [document = false]
  sessions
    Lib
    "HOL-Eisbach"
  directories
    "$L4V_ARCH"
    "../machine"
    "../machine/$L4V_ARCH"
  theories
    "API_H"
    "$L4V_ARCH/ArchIntermediate_H"


(*
 * C Kernel
 *)

session CSpec in "cspec" = CKernel +
  directories
    "c/build/$L4V_ARCH/generated/arch/object"
    "c/build/$L4V_ARCH/generated/sel4"
  theories [condition = "SORRY_MODIFIES_PROOFS", quick_and_dirty]
    "Substitute"
  theories [condition = "SORRY_BITFIELD_PROOFS", quick_and_dirty]
    "KernelInc_C"
  theories
    "KernelInc_C"
    "KernelState_C"

session CKernel in "cspec/$L4V_ARCH" = CParser +
  sessions
    "ExecSpec"
    "CLib"
    "AsmRefine"
  theories [condition = "SORRY_MODIFIES_PROOFS", quick_and_dirty]
    "Kernel_C"
  theories
    "Kernel_C"


(*
 * CapDL
 *)

session DSpec in capDL = Word_Lib +
  sessions
    ExecSpec
    ASpec
  theories
    Syscall_D


(*
 * Take-Grant.
 *)

session TakeGrant in "take-grant" = Word_Lib +
  theories
    "System_S"
    "Isolation_S"
    "Example"
    "Example2"


(*
 * Separation Kernel Setup Specification
 *)

session ASepSpec in "sep-abstract" = ASpec +
  options [document = false]
  theories
    "Syscall_SA"

